The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^3)).

0 CpxTRS
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
↳2 CdtProblem
↳3 CdtGraphRemoveTrailingProof (BOTH BOUNDS(ID, ID))
↳4 CdtProblem
↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))
↳6 CdtProblem
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))
↳8 CdtProblem
↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^3))))
↳10 CdtProblem
↳11 SIsEmptyProof (⇔)
↳12 BOUNDS(O(1), O(1))

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

ite(tt, u, v) → u
ite(ff, u, v) → v
find(u, v, nil) → ff
find(u, v, cons(cons(u, v), E)) → tt
find(u, v, cons(cons(u2, v2), E)) → find(u, v, E)
complete(u, nil, E) → tt
complete(u, cons(v, S), E) → ite(find(u, v, E), complete(u, S, E), ff)
clique(nil, E) → tt
clique(cons(u, K), E) → ite(complete(u, K, E), clique(K, E), ff)

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

ite(tt, z0, z1) → z0
ite(ff, z0, z1) → z1
find(z0, z1, nil) → ff
find(z0, z1, cons(cons(z0, z1), z2)) → tt
find(z0, z1, cons(cons(z2, z3), z4)) → find(z0, z1, z4)
complete(z0, nil, z1) → tt
complete(z0, cons(z1, z2), z3) → ite(find(z0, z1, z3), complete(z0, z2, z3), ff)
clique(nil, z0) → tt
clique(cons(z0, z1), z2) → ite(complete(z0, z1, z2), clique(z1, z2), ff)
Tuples:

FIND(z0, z1, cons(cons(z2, z3), z4)) → c4(FIND(z0, z1, z4))
COMPLETE(z0, cons(z1, z2), z3) → c6(ITE(find(z0, z1, z3), complete(z0, z2, z3), ff), FIND(z0, z1, z3), COMPLETE(z0, z2, z3))
CLIQUE(cons(z0, z1), z2) → c8(ITE(complete(z0, z1, z2), clique(z1, z2), ff), COMPLETE(z0, z1, z2), CLIQUE(z1, z2))
S tuples:

FIND(z0, z1, cons(cons(z2, z3), z4)) → c4(FIND(z0, z1, z4))
COMPLETE(z0, cons(z1, z2), z3) → c6(ITE(find(z0, z1, z3), complete(z0, z2, z3), ff), FIND(z0, z1, z3), COMPLETE(z0, z2, z3))
CLIQUE(cons(z0, z1), z2) → c8(ITE(complete(z0, z1, z2), clique(z1, z2), ff), COMPLETE(z0, z1, z2), CLIQUE(z1, z2))
K tuples:none
Defined Rule Symbols:

ite, find, complete, clique

Defined Pair Symbols:

FIND, COMPLETE, CLIQUE

Compound Symbols:

c4, c6, c8

(3) CdtGraphRemoveTrailingProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing tuple parts

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

ite(tt, z0, z1) → z0
ite(ff, z0, z1) → z1
find(z0, z1, nil) → ff
find(z0, z1, cons(cons(z0, z1), z2)) → tt
find(z0, z1, cons(cons(z2, z3), z4)) → find(z0, z1, z4)
complete(z0, nil, z1) → tt
complete(z0, cons(z1, z2), z3) → ite(find(z0, z1, z3), complete(z0, z2, z3), ff)
clique(nil, z0) → tt
clique(cons(z0, z1), z2) → ite(complete(z0, z1, z2), clique(z1, z2), ff)
Tuples:

FIND(z0, z1, cons(cons(z2, z3), z4)) → c4(FIND(z0, z1, z4))
COMPLETE(z0, cons(z1, z2), z3) → c6(FIND(z0, z1, z3), COMPLETE(z0, z2, z3))
CLIQUE(cons(z0, z1), z2) → c8(COMPLETE(z0, z1, z2), CLIQUE(z1, z2))
S tuples:

FIND(z0, z1, cons(cons(z2, z3), z4)) → c4(FIND(z0, z1, z4))
COMPLETE(z0, cons(z1, z2), z3) → c6(FIND(z0, z1, z3), COMPLETE(z0, z2, z3))
CLIQUE(cons(z0, z1), z2) → c8(COMPLETE(z0, z1, z2), CLIQUE(z1, z2))
K tuples:none
Defined Rule Symbols:

ite, find, complete, clique

Defined Pair Symbols:

FIND, COMPLETE, CLIQUE

Compound Symbols:

c4, c6, c8

(5) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

CLIQUE(cons(z0, z1), z2) → c8(COMPLETE(z0, z1, z2), CLIQUE(z1, z2))
We considered the (Usable) Rules:none
And the Tuples:

FIND(z0, z1, cons(cons(z2, z3), z4)) → c4(FIND(z0, z1, z4))
COMPLETE(z0, cons(z1, z2), z3) → c6(FIND(z0, z1, z3), COMPLETE(z0, z2, z3))
CLIQUE(cons(z0, z1), z2) → c8(COMPLETE(z0, z1, z2), CLIQUE(z1, z2))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CLIQUE(x1, x2)) = [2]x1 + x1·x2   
POL(COMPLETE(x1, x2, x3)) = [3] + x3   
POL(FIND(x1, x2, x3)) = 0   
POL(c4(x1)) = x1   
POL(c6(x1, x2)) = x1 + x2   
POL(c8(x1, x2)) = x1 + x2   
POL(cons(x1, x2)) = [2] + x2   

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

ite(tt, z0, z1) → z0
ite(ff, z0, z1) → z1
find(z0, z1, nil) → ff
find(z0, z1, cons(cons(z0, z1), z2)) → tt
find(z0, z1, cons(cons(z2, z3), z4)) → find(z0, z1, z4)
complete(z0, nil, z1) → tt
complete(z0, cons(z1, z2), z3) → ite(find(z0, z1, z3), complete(z0, z2, z3), ff)
clique(nil, z0) → tt
clique(cons(z0, z1), z2) → ite(complete(z0, z1, z2), clique(z1, z2), ff)
Tuples:

FIND(z0, z1, cons(cons(z2, z3), z4)) → c4(FIND(z0, z1, z4))
COMPLETE(z0, cons(z1, z2), z3) → c6(FIND(z0, z1, z3), COMPLETE(z0, z2, z3))
CLIQUE(cons(z0, z1), z2) → c8(COMPLETE(z0, z1, z2), CLIQUE(z1, z2))
S tuples:

FIND(z0, z1, cons(cons(z2, z3), z4)) → c4(FIND(z0, z1, z4))
COMPLETE(z0, cons(z1, z2), z3) → c6(FIND(z0, z1, z3), COMPLETE(z0, z2, z3))
K tuples:

CLIQUE(cons(z0, z1), z2) → c8(COMPLETE(z0, z1, z2), CLIQUE(z1, z2))
Defined Rule Symbols:

ite, find, complete, clique

Defined Pair Symbols:

FIND, COMPLETE, CLIQUE

Compound Symbols:

c4, c6, c8

(7) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

COMPLETE(z0, cons(z1, z2), z3) → c6(FIND(z0, z1, z3), COMPLETE(z0, z2, z3))
We considered the (Usable) Rules:none
And the Tuples:

FIND(z0, z1, cons(cons(z2, z3), z4)) → c4(FIND(z0, z1, z4))
COMPLETE(z0, cons(z1, z2), z3) → c6(FIND(z0, z1, z3), COMPLETE(z0, z2, z3))
CLIQUE(cons(z0, z1), z2) → c8(COMPLETE(z0, z1, z2), CLIQUE(z1, z2))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CLIQUE(x1, x2)) = [2]x12   
POL(COMPLETE(x1, x2, x3)) = [3] + [2]x2   
POL(FIND(x1, x2, x3)) = 0   
POL(c4(x1)) = x1   
POL(c6(x1, x2)) = x1 + x2   
POL(c8(x1, x2)) = x1 + x2   
POL(cons(x1, x2)) = [2] + x2   

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

ite(tt, z0, z1) → z0
ite(ff, z0, z1) → z1
find(z0, z1, nil) → ff
find(z0, z1, cons(cons(z0, z1), z2)) → tt
find(z0, z1, cons(cons(z2, z3), z4)) → find(z0, z1, z4)
complete(z0, nil, z1) → tt
complete(z0, cons(z1, z2), z3) → ite(find(z0, z1, z3), complete(z0, z2, z3), ff)
clique(nil, z0) → tt
clique(cons(z0, z1), z2) → ite(complete(z0, z1, z2), clique(z1, z2), ff)
Tuples:

FIND(z0, z1, cons(cons(z2, z3), z4)) → c4(FIND(z0, z1, z4))
COMPLETE(z0, cons(z1, z2), z3) → c6(FIND(z0, z1, z3), COMPLETE(z0, z2, z3))
CLIQUE(cons(z0, z1), z2) → c8(COMPLETE(z0, z1, z2), CLIQUE(z1, z2))
S tuples:

FIND(z0, z1, cons(cons(z2, z3), z4)) → c4(FIND(z0, z1, z4))
K tuples:

CLIQUE(cons(z0, z1), z2) → c8(COMPLETE(z0, z1, z2), CLIQUE(z1, z2))
COMPLETE(z0, cons(z1, z2), z3) → c6(FIND(z0, z1, z3), COMPLETE(z0, z2, z3))
Defined Rule Symbols:

ite, find, complete, clique

Defined Pair Symbols:

FIND, COMPLETE, CLIQUE

Compound Symbols:

c4, c6, c8

(9) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^3))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

FIND(z0, z1, cons(cons(z2, z3), z4)) → c4(FIND(z0, z1, z4))
We considered the (Usable) Rules:none
And the Tuples:

FIND(z0, z1, cons(cons(z2, z3), z4)) → c4(FIND(z0, z1, z4))
COMPLETE(z0, cons(z1, z2), z3) → c6(FIND(z0, z1, z3), COMPLETE(z0, z2, z3))
CLIQUE(cons(z0, z1), z2) → c8(COMPLETE(z0, z1, z2), CLIQUE(z1, z2))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CLIQUE(x1, x2)) = x12·x2   
POL(COMPLETE(x1, x2, x3)) = x2·x3   
POL(FIND(x1, x2, x3)) = x3 + x2·x3   
POL(c4(x1)) = x1   
POL(c6(x1, x2)) = x1 + x2   
POL(c8(x1, x2)) = x1 + x2   
POL(cons(x1, x2)) = [1] + x1 + x2   

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

ite(tt, z0, z1) → z0
ite(ff, z0, z1) → z1
find(z0, z1, nil) → ff
find(z0, z1, cons(cons(z0, z1), z2)) → tt
find(z0, z1, cons(cons(z2, z3), z4)) → find(z0, z1, z4)
complete(z0, nil, z1) → tt
complete(z0, cons(z1, z2), z3) → ite(find(z0, z1, z3), complete(z0, z2, z3), ff)
clique(nil, z0) → tt
clique(cons(z0, z1), z2) → ite(complete(z0, z1, z2), clique(z1, z2), ff)
Tuples:

FIND(z0, z1, cons(cons(z2, z3), z4)) → c4(FIND(z0, z1, z4))
COMPLETE(z0, cons(z1, z2), z3) → c6(FIND(z0, z1, z3), COMPLETE(z0, z2, z3))
CLIQUE(cons(z0, z1), z2) → c8(COMPLETE(z0, z1, z2), CLIQUE(z1, z2))
S tuples:none
K tuples:

CLIQUE(cons(z0, z1), z2) → c8(COMPLETE(z0, z1, z2), CLIQUE(z1, z2))
COMPLETE(z0, cons(z1, z2), z3) → c6(FIND(z0, z1, z3), COMPLETE(z0, z2, z3))
FIND(z0, z1, cons(cons(z2, z3), z4)) → c4(FIND(z0, z1, z4))
Defined Rule Symbols:

ite, find, complete, clique

Defined Pair Symbols:

FIND, COMPLETE, CLIQUE

Compound Symbols:

c4, c6, c8

(11) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(12) BOUNDS(O(1), O(1))